perm filename AX32S[1,JRA] blob sn#005856 filedate 1972-07-21 generic text, type T, neo UTF8
00100	(LE(ADD1(J) X1) ∧ LE(X1 SUB1(CN))) → LE(A(X1) A(ADD1(X1)));
00200	(LE(U X1) ∧ LE( X1 SUB1(I)) ∧ LE(SUB1(I) CN))→ LE(A(X1) BIG);
00300	(LE(U X1) ∧ LE(X1 J) ∧ LE(J SUB1 (CN))) → LE(A(X1) A(ADD1(J)));
00400	E(BIG A(LOC));
00450	LE(U LOC) ∧ LE(LOC J) ;
00500	LE(ADD1 (U) I);
00600	E(LOC J);
00700	LE(ADD1(J) I);
00800	LE(ADD1 (U) J) ∧ LE(J CN);
00900	;
01000